When producing or consuming a QP, evalQuantified first evaluates and assumes the QP's condition. This condition could of course be unsatisfiable, in which case producing or consuming the QP should not affect the state and verification should continue.

Currently, however, the following is possible:

• The QP's condition is unsatisfiable, thus evalQuantified locally assumes false (as it should)
• When evaluating the argument and permission amount expressions of the QP, a smoke check is triggered and succeeds, in which case no value is returned and the continuation of this evaluation is never invoked.
• Since the continuation of evalQuantified itself is invoked only from said continuation, verification just stops at this point, and any subsequent conjuncts are never produced/consumed and any subsequent statements never executed. This is obviously unsound (see issue Unsoundness related to QPs with unsatisfiable conditions #842 for an example), since only the path in the quantifier where its condition is true was unreachable, not the entire path the quantifier is on.

This PR changes evalQuantified s.t. its continuation is always called, now with an optional result to tell the caller if the above scenario happened and the quantifier is therefore trivially satisfied.